λxyz.xz(yz) 是λ微积分中的抽象还是应用？

Question

根据 lambda 演算，λxyz.xz(yz) 应该被视为 λxyz.xz 对 (yz) 的应用还是 xz(yz) 中的括号简单意味着操作应该去像 (xz)(yz) 而不是 ((xz)y)z 并且整个 xz(yz) 都在函数 "body" 中？

我认为这是一个抽象，应用程序必须像 (λxyz.xz)yz 那样编写，但我的理解很差所以我想检查一下。

Answer 1

正确。确切地说，这取决于 lambda 项语法的确切定义，更准确地说是括号省略规则，但这些规则有约定俗成。特别是，通常

申请优先于抽象，所以你首先尝试形成 xz 到 yz 的应用，然后才 x、y 和 z 上的抽象，而不是首先形成抽象 λxyz.xz，然后将生成的术语嵌入到 yz 的应用程序中（这就是如果抽象优先于应用程序，你会得到）；
应用术语中的括号是左结合的，因此 xzyz（yz 周围没有括号）将被读作 ((xz)y)z，并表示 xz 是应用于 yz，您需要将术语 yz.

因此，正如您所怀疑的，λxyz.xz(yz) 是 xz(yz) 的三重抽象，它本身是 xz 到 yz 的应用，这又是应用分别是 x 到 z 和 y 到 z。

所有括号都存在，术语是 λx.(λy.(λz.(xz(yz))))。
因此，该术语的语法树如下所示：

λxyz.xz(yz): abstraction
|- x: variable
|- λyz.xz(yz): abstraction
  |- y: variable
  |- λz.xz(yz): abstraction
     |- z: variable
     |- xz(yz): application
        |- xz: application
        |  |- x: variable
        |  |- z: variable
        |- yz: application
           |- y: variable
           |- z: variable

正如您所猜想的那样，λxyz.xz 对 yz 的应用将写为 (λxyz.xz)yz。

λxyz.xz(yz) 是λ微积分中的抽象还是应用？

Is λxyz.xz(yz) an abstraction or an application in Lambda Calculus?

lambda-calculus